Refinement-based Specification and Security Analysis of Separation Kernels

摘要

Assurance of information-flow security by formal methods is mandated insecurity certification of separation kernels. As an industrial standard forimproving safety, ARINC 653 has been complied with by mainstream separationkernels. Due to the new trend of integrating safe and secure functionalitiesinto one separation kernel, security analysis of ARINC 653 as well as a formalspecification with security proofs are thus significant for the development andcertification of ARINC 653 compliant Separation Kernels (ARINC SKs). This paperpresents a specification development and security analysis method for ARINC SKsbased on refinement. We propose a generic security model and a stepwiserefinement framework. Two levels of functional specification are developed bythe refinement. A major part of separation kernel requirements in ARINC 653 aremodeled, such as kernel initialization, two-level scheduling, partition andprocess management, and inter-partition communication. The formal specificationand its security proofs are carried out in the Isabelle/HOL theorem prover. Wehave reviewed the source code of one industrial and two open-source ARINC SKimplementations, i.e. VxWorks 653, XtratuM, and POK, in accordance with theformal specification. During the verification and code review, six securityflaws, which can cause information leakage, are found in the ARINC 653 standardand the implementations.